package sat;

import java.util.HashMap;
import java.util.Vector;
import sat.exceptions.ParseException;

/**
 *
 * @author bawey
 */
public class ClauseCNF {

    private Vector<LiteralCNF> literals;

    /**
     * @param representation formuła logiczna w postaci CNF
     * @throws ParseException 
     */
    public ClauseCNF(String representation) throws ParseException {
        literals = new Vector<LiteralCNF>();
        parseString(representation);
    }

    /**
     * @return liczba literałów w klauzuli
     */
    public int getLiteralsCount() {
        return literals.size();
    }

    /**
     * @return Vector literałów występujących w klauzuli, pomija ew. negację
     */
    public Vector<String> getStringLiterals() {
        Vector<String> temp = new Vector<String>();
        for (int i = 0; i < literals.size(); ++i) {
            temp.add(literals.get(i).getSymbol());
        }
        return temp;
    }

    /**
     * Sprawdza, czy dla danego podstawienia klauzula jest prawdziwa
     * @param values - podstawienia
     * @return 
     */
    public boolean evaluate(HashMap<String, Boolean> values) {
        for (int i = 0; i < literals.size(); ++i) {
            //what will return without entry?
            if ((values.get(literals.get(i).getSymbol())).booleanValue() ^ literals.get(i).isNegated()) {
                return true;
            }
        }
        return false;
    }

    /**
     * Funkcja prywatna, konwertuje klauzulę z postaci tekstowej do reprezentacji wewnętrznej
     * @param c tekst wejściowy
     * @throws ParseException 
     */
    private void parseString(String c) throws ParseException {
        c = StringToolkit.strip(c);
        boolean negated = false;
        StringBuffer literal = new StringBuffer();
        for (int i = 0; i < c.length(); ++i) {
            if (c.charAt(i) == '~') {
                if (literal.length() == 0) {
                    negated = !negated;
                } else {
                    throw (new ParseException("unexpected ~"));
                }
            } else if (c.charAt(i) == '|') {
                if (literal.length() > 0) {
                    literals.add(new LiteralCNF(literal.toString(), negated));
                    literal = new StringBuffer();
                    negated = false;
                } else {
                    throw (new ParseException("unexpected |"));
                }
            } else {
                literal.append(c.charAt(i));
            }
        }
        if (literal.length() > 0) {
            literals.add(new LiteralCNF(literal.toString(), negated));
        }
    }

    public String toString() {
        StringBuffer sb = new StringBuffer();
        sb.append("(");
        for (int i = 0; i < literals.size(); ++i) {
            if (i != 0) {
                sb.append("|");
            }
            sb.append(literals.get(i).toString());
        }
        sb.append(")");
        return sb.toString();
    }
}
